Prove termination of diff algorithm implementation - #37

A `_wfDistanceToGoal` function is defined to be used as termination metric
for `ses`. In this commit, `dstep` is specified and checked to reduce it
from input to output.

The wave front diagonal condition is changed to look at the head
of the node list instead of the diagonal edit distance parameter,
and its nodes are specified to be within bounds.
Indeed, now that wave fronts are trimmed down to be within bounds,
we can no longer guarantee that the first node's diagonal matches
the edit distance.

The `stepAndMerge` specification is strengthen to preserve this new variant of
wave front diagonal invariant: With the current optimization of `dstep`,
wave fronts don't necessarily grow, but the 2-step specing is preserved.

The implementation of `ses` changes from a `dropWhile` driven search for
the algorithm's end point in a lazy stream composed of all wave front nodes,
to the explicit recursion of a wave-front wise search for such end point.

This change was designed to allow a termination proof using Liquid Haskell:
by inspecting each wave front separately, instead of all concatenated together in an
infinite stream, we can define a wave front metric as its minimum distance to
the endpoint and show it is reduced by the recursive calls (to `dstep`).

Performance-wise, we get a small optimization of the benchmark of ~12%

…Goal`

…eason#28)

The optimization introduced in `dstep` (narrowing the wave front to only
within bound nodes) solves the problem this additional equations addressed
in seereason@33bf8bc
They are removed to avoid unnecessary complexity.

A definition less, plus upstream has an optimization for `const`
in ucsd-progsys/liquidhaskell#2732
that could turn out to be useful (currently is makes no
difference because lemmas are not being composed).